i, j:. ((i = j) ~ ff)  i  j 

latex

ProofTree

Definitions	t  T, x:A. B(x), P  Q, a  b  T , , P & Q, P  Q
Lemmas	int sq, bfalse wf, assert of eq int, not functionality wrt iff, assert of bnot, eqff to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf